COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	
C00003 00003	
C00005 ENDMK
C⊗;


STANFORD ARTIFICIAL INTELLIGENCE LABORATORY           SEPTEMBER 1973
OPERATING NOTE 73







.BEGIN CENTER





PRELIMINARY USER'S MANUAL
FOR
AN
INTERACTIVE THEOREM PROVER

BY

JOHN ALLEN
.END










ABSTRACT:


.BEGIN DOUBLE SPACE
This document represents a short guide to using the theorem prover.  An earlier
version of this program is described in Allen and Luckham [MI5].  
Many of the later sections of this manual,
on pattern matching and subroutining especially, are still in a rudimentary
stage of development. Experiments demonstrating various applications of the strategies
and the user oriented features are described in a forthcoming report,
"Applications of First Order Proof Procedures" by Allen, Luckham, and Morales.
.END
.SKIP 10
This work was supported in part by the Advanced Research Projects Agency of the
Office of the Secretary of Defense under Contract No. DAHC15-73-C-0435.